Collaborative work on shared documents was revolutionized by web services like Google Docs or Etherpad. Multiple users can work on the same document in a comfortable and distributed way. For the synchronization of the changes a repli- cation system named Operational Transformation is used. Such a system consists of a control algorithm and a transformation function. In essence, a transformation function solves the conflicts that arise when multiple users change the document at the same time. In this work we investigate on the correctness of such transfor- mation functions. We introduce transformation functions for graphs and trees so that such structures can be manipulated by multiple users in a collaborative way. In order to prove the correctness of the transformation functions we mostly use the interactive theorem prover Isabelle/HOL to verify the necessary properties.